Nuprl Lemma : causal_order_or 4,23
T:Type, L:T List, R:(||L||||L||Prop), P1, P2, P3:(||L||Prop).
(Trans _1,_2:||L||. R(_1,_2))
 causal_order(L;R;P1;P2)
 causal_order(L;R;P1;P3)
 causal_order(L;R;P1;i.P2(i)  P3(i)) 
latex

Definitionst  T, {i..j}, x:A. B(x), AB, Prop, P & Q, x:A. B(x), P  Q, P  Q, ||as||, x,y. t(x;y), Trans x,y:T. E(x;y), False, A, i  j < k, causal_order(L;R;P;Q)
Lemmastrans wf, int seg wf, length wf1, le wf

origin